/******************************************************************************

    Copyright (C) 2010-2011 Alessio Stalla (alessiostalla@gmail.com)

    This file is part of PrettyProlog.

    PrettyProlog is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 3 of the License, or
    (at your option) any later version.

    PrettyProlog is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PrettyProlog; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA

    See the file COPYING for further details.

 *****************************************************************************/


package prettyprolog.parser;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.Reader;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.Scanner;

import org.parboiled.Action;
import org.parboiled.BaseParser;
import org.parboiled.Context;
import org.parboiled.MatcherContext;
import org.parboiled.Parboiled;
import org.parboiled.Rule;
import org.parboiled.annotations.BuildParseTree;
import org.parboiled.common.StringUtils;
import org.parboiled.errors.ActionException;
import org.parboiled.errors.InvalidInputError;
import org.parboiled.errors.ParseError;
import org.parboiled.matchers.FirstOfMatcher;
import org.parboiled.matchers.Matcher;
import org.parboiled.parserunners.ParseRunner;
import org.parboiled.parserunners.ReportingParseRunner;
import org.parboiled.support.DefaultValueStack;
import org.parboiled.support.MatcherPath;
import org.parboiled.support.ParsingResult;
import org.parboiled.support.ToStringFormatter;
import org.parboiled.trees.GraphNode;
import org.parboiled.trees.GraphUtils;

import prettyprolog.datatypes.Callable;
import prettyprolog.datatypes.CharString;
import prettyprolog.datatypes.Cons;
import prettyprolog.datatypes.Constant;
import prettyprolog.datatypes.Namespace;
import prettyprolog.datatypes.Nil;
import prettyprolog.datatypes.Real;
import prettyprolog.datatypes.Symbol;
import prettyprolog.datatypes.Term;
import prettyprolog.datatypes.Variable;
import prettyprolog.engine.Clause;
import prettyprolog.engine.Goal;
import prettyprolog.engine.Theory;

@BuildParseTree
public class Parser extends BaseParser<Object> {

	protected final Symbol clauseSymbol;
	
	public static Parser makeInstance() {
	    return Parboiled.createParser(Parser.class);
	}
	
	protected Parser() {
		this.clauseSymbol = Namespace.current().intern(":-"); //Not infix - someone else will do it
	}

	public Rule Theory() {
		return Sequence(OneOrMore(ZeroOrMore(Comment()), Clause(), pushClauseToTheory()), ZeroOrMore(Comment()), EOI);
	}
	
	public Rule Goal() {
		return Sequence(Term(),	ZeroOrMore(',', Term()), '.', pushGoal());
	}
	
	public Rule Clause() {
		//TODO ammettere costanti come clausole? l'algoritmo di risoluzione non lo supporta per ora
		return Sequence(ZeroOrMore(WhiteSpace()),
						FirstOf(Sequence(ClauseSymbol(), ZeroOrMore(WhiteSpace()), Callable(), pushDirective()),
								Sequence(Callable(), pushClause())),
						ZeroOrMore(WhiteSpace()), '.');
	}
	
	public Rule TermPlusDot() {
		return Sequence(Term(), '.');
	}
	
	public Rule Term() {
		return //FirstOf(Sequence(ZeroOrMore(WhiteSpace()), '(', Term(), ')', ZeroOrMore(WhiteSpace())),
					   Sequence(ZeroOrMore(WhiteSpace()), FirstOf(Callable(), List(), Atom()), ZeroOrMore(WhiteSpace()));//);
	}
	
	public Rule Atom() {
		return FirstOf(Number(), CharString(), Variable(), Constant());
	}
		
	public Rule Callable() {
		return FirstOf(Sequence(OpenParen(), Term(), CloseParen(), checkInfixCallable(), ZeroOrMore(InfixCallableAux())), //(a + b) * c
					   InfixCallable(), //a + b
					   PrefixCallable()); //foo(bar, baz)
	}

	public Rule InfixCallable() {
		return OneOrMore(Sequence(FirstOf(List(), PrefixCallable(), Atom()), InfixCallableAux()));
	}

	public Rule PrefixCallable() {
		return Sequence(FirstOf(Sequence(Symbol(), ZeroOrMore(WhiteSpace()), OpenParen()), Sequence(OpenParen(), push(null))),
						ZeroOrMore(Term(), ZeroOrMore(',', Term())),
						CloseParen(),
						pushPrefixCallable());
	}
	
	//TODO left-associative infix ops!!!
	public Rule InfixCallableAux() { //First token already parsed by Callable()
		return FirstOf(Sequence(ZeroOrMore(WhiteSpace()), ClauseSymbol(), Term(), ZeroOrMore(',', Term()), pushInfixCallable()),
					   Sequence(ZeroOrMore(WhiteSpace()), Symbol(), checkInfix(), Term(), pushInfixCallable()));
	}
	
	protected static final Object LIST_START = new Object();
	
	public Rule List() {
		return Sequence('[', ZeroOrMore(WhiteSpace()),
						FirstOf(Sequence(push(LIST_START), Term(), ZeroOrMore(Sequence(',', Term())), pushList(),
								         Optional('|', Term(), push(makeCons()))), //CDR
						        push(Nil.NIL)),
				        ']');
	}
	
	protected Cons makeCons() {
		Term rest = (Term) pop();
		Cons cons = (Cons) pop();
		Term cdr = cons;
		while(cdr != Nil.NIL) {
			if(cdr instanceof Cons) {
				if(((Cons) cdr).cdr() == Nil.NIL) {
					((Cons) cdr).setCdr(rest);
					return cons;
				} else {
					cdr = ((Cons) cdr).cdr();
				}
			} else {
				throw new IllegalStateException("Malformed list: " + cons + " | " + rest);
			}
		}
		return cons;
	}
	
	protected boolean pushList() { //X = [a, b, [1,2] | (1, 2, 3)].
		Term c = Nil.NIL;
		Object o;
		while((o = pop()) != LIST_START) {
			c = new Cons((Term) o, c);
		}
		return push(c);
	}
	
	public static final Action<Object> PRINT = new Action<Object>() {

		public boolean run(Context<Object> ctx) {
			System.out.println("DEBUG " + ctx);
			return true;
		}
	};
	
	public boolean println(String s) {
		System.out.println(s);
		return true;
	}
	
	public Rule ClauseSymbol() {
		return Sequence(":-", push(clauseSymbol));
	}
	
	public Matcher InfixSymbol() {
		return new FirstOfMatcher(new Rule[0]) {
			
			@SuppressWarnings({ "unchecked", "rawtypes" })
			@Override
			public boolean match(MatcherContext context) {
				for(Symbol s : Namespace.getInfixSymbols()) {
					if (context.getInputBuffer().test(context.getCurrentIndex(), s.getName().toCharArray())) {
			        	context.advanceIndex(s.getName().length());
			        	context.createNode();
			        	context.getValueStack().push(s);
			        	return true;
			        }
				}
				return false;
			}
			
		};
	}
		
	public Rule Symbol() {
	    return FirstOf(Sequence(InfixSymbol(), FirstOf(checkTerminating(), Test(Separator()))),
	                   Sequence(Sequence(TestNot(Separator()), ANY, ContinueSymbol()), pushSymbol(match())));
	}

    public Rule ContinueSymbol() {
		return ZeroOrMore(TestNot(Separator()), TestNot(InfixSymbol(), checkTerminating()), ANY);
	}
    
    protected final Action<Object> PUSH_SYMBOL = new Action<Object>() {

        public boolean run(Context<Object> ctx) {
            int colonIndex = ctx.getMatch().indexOf(':');
            if(colonIndex >= 0) {
                String namespaceName = ctx.getMatch().substring(0, colonIndex);
                Namespace namespace = Namespace.get(namespaceName);
                if(namespace == null) {
                    ((MatcherContext<Object>) ctx).markError();
                    ctx.getParseErrors().add(new InvalidInputError(ctx.getInputBuffer(), ctx.getMatchStartIndex(), new ArrayList<MatcherPath>(), "Nonexistent Symbol Table: " + namespaceName));
                    return false; //TODO
                    //throw new InvalidInputError("Nonexistent Symbol Table: " + symbolTableName);
                }
                return push(namespace.intern(ctx.getMatch().substring(colonIndex + 1)));
            } else {
                return push(Namespace.current().intern(ctx.getMatch()));
            }
        }
    };
    
    protected boolean pushSymbol(String match) {
        int colonIndex = match.indexOf(':');
        if(colonIndex >= 0) {
            String namespaceName = match.substring(0, colonIndex);
            Namespace namespace = Namespace.get(namespaceName);
            if(namespace == null) {
                System.err.println("Nonexistent namespace: " + namespaceName);
                return false; //TODO
                //throw new InvalidInputError("Nonexistent Symbol Table: " + symbolTableName);
            }
            return push(namespace.intern(match.substring(colonIndex + 1)));
        } else {
            return push(Namespace.current().intern(match));
        }
    }


	public Rule OpenParen() {
		return Sequence('(', ZeroOrMore(WhiteSpace()));
	}
	
	public Rule CloseParen() {
		return Sequence(ZeroOrMore(WhiteSpace()), ')');
	}
	
	public Rule Variable() {
		return Sequence(Sequence(FirstOf('_', CharRange('A', 'Z')), ContinueSymbol()),
				        push(new Variable(Namespace.current().intern(match()))));
	}
	
	public Rule Constant() {
		return Sequence(Symbol(), push(new Constant((Symbol) pop())));
	}
	
	public Rule Separator() {
		return FirstOf(WhiteSpace(), '.', ',', '(', ')', '[', ']', '|', '\'', EOI);
	}
		
	public Rule WhiteSpace() {
		return FirstOf(' ', '\t', '\r', '\n');
	}
	
	public Rule Number() {
		return FirstOf(Real(), Integer());
	}
	
	public Rule CharString() {
		return Sequence('\'', ZeroOrMore(TestNot('\''), ANY), push(new CharString(match())), '\''); //TODO escape
	}
	
	public Rule Integer() {
        return Sequence(Optional(FirstOf('+', '-')), OneOrMore(Digit()),
        				push(new Real(Integer.parseInt(match()))));
    }
	
	public Rule Real() {
        return Sequence(Sequence(Optional(FirstOf('+', '-')), OneOrMore(Digit()), Optional(Sequence('.', OneOrMore(Digit())))),
        			    push(new Real(Double.parseDouble(match()))));
    }
	
    public Rule Digit() {
        return CharRange('0', '9');
    }
    
    public Rule Comment() {
    	return Sequence(ZeroOrMore(WhiteSpace()), '%', ZeroOrMore(TestNot('\n'), ANY), '\n');
    }
    
    public Theory parseTheory(Theory th, Reader r) throws IOException, ParseException {
    	StringWriter w = new StringWriter();
    	BufferedReader rr = new BufferedReader(r);
    	int i;
    	char[] buf = new char[4096];
    	while((i = rr.read(buf)) != -1) {
    		w.append(new String(buf, 0, i));
    	}
    	String input = w.toString().trim();
        if (StringUtils.isEmpty(input)) {
        	return null;
        }
        DefaultValueStack<Theory> stack = new DefaultValueStack<Theory>();
        stack.push(th);
        ParseRunner<Theory> runner = new ReportingParseRunner<Theory>(Theory()).withValueStack(stack);
        return parse(runner, input);
    }
    
    public Object parse(Rule r, String input) throws ParseException {
    	ParseRunner<Object> runner = new ReportingParseRunner<Object>(r);
        return parse(runner, input);
    }

	public <T> T parse(ParseRunner<T> runner, String input) {
		ParsingResult<T> result = runner.run(input);
        if(!result.hasErrors()) {
        	return result.resultValue;
        } else {
        	ParseError p = result.parseErrors.get(0);
        	int st = p.getStartIndex();
        	int end = p.getEndIndex();
        	int sst = Math.max(0, st - 10);
        	int send = Math.min(input.length(), end + 10);
        	String substr = input.substring(sst, send);
        	if(sst > 0) {
        		substr = "..." + substr;
        	}
        	if(send < input.length()) {
        		substr = substr + "...";
        	}
        	throw new ParseException(p + " (" + p.getErrorMessage() + ") at " + st + " - " + end + " (\"" + substr + "\")");
        }
	}
    
    protected boolean pushPrefixCallable() {
		List<Term> args = new ArrayList<Term>();
		while(true) {
			Object o = pop();
			if(o instanceof Term) {
				args.add(0, (Term) o);
			} else if(o instanceof Symbol || o == null) {
				push(new Callable((Symbol) o, args));
				return true;
			} else {
				throw new ActionException("Unexpected token in callable: " + o);
			}
		}
	}

	protected boolean pushInfixCallable() {
		List<Term> args = new ArrayList<Term>();
		Object o;
		while(!((o = pop()) instanceof Symbol)) {
			args.add(0, (Term) o);
		}
		Symbol sym = (Symbol) o;
		o = pop();
		args.add(0, (Term) o);
		if(sym.isInfix()) {
			push(new Callable((Symbol) sym, args));
		} else {
			throw new ActionException("Non infix symbol found in infix position: " + sym);
		}
		return true;
	}
	
	protected boolean pushDirective() {
		Clause cl = new Clause(null, Arrays.asList(new Term[] { (Callable) pop() }));
		pop(); //To remove the clause symbol
		return push(cl);
	}
	
	protected boolean pushClause() {
		return push(new Clause((Callable) pop(), clauseSymbol));
	}
	
	protected boolean pushClauseToTheory() {
		Clause c = (Clause) pop();
		Theory th = (Theory) peek();
		try {
		    th.assertz(c);
		    return true;
		} catch(Exception e) { //In case c is a directive and it fails for some reason
		    e.printStackTrace();
		    return false; //TODO explain to user
		}
	}
	
	protected boolean pushGoal() {
		Goal g = new Goal();
		while(true) {
			try {
				g.add(0, (Term) pop());
			} catch(IllegalArgumentException e) {
				break; //stack is empty
			}
		}
		push(g);
		return true;
	}
	
	protected boolean checkInfix() {
		Symbol sym = (Symbol) peek();
		if(sym.isInfix()) {
			return true;
		} else {
			return false;
		}
	}
	
	protected boolean checkTerminating() {
		Symbol sym = (Symbol) peek();
		if(sym.isTerminating()) {
			return true;
		} else {
			return false;
		}
	}
	
	protected boolean checkInfixCallable() {
		Term t = (Term) pop();
		if(t instanceof Callable) {
			Callable c = (Callable) t;
			boolean b = c.getSymbol() != null && c.getSymbol().isInfix();
			if(b) {
				push(c);
			}
			return b;
		} else {
			return false;
		}
	}
	
	@SuppressWarnings({ "unchecked", "rawtypes" })
	public static void main(String[] args) {
		Namespace namespace = new Namespace("parser_test");
		namespace.internInfix("==");
		namespace.internInfix("=");
		namespace.internInfix("\\=");
		namespace.internInfix("\\==");
		namespace.internInfix(":-");
		namespace.internInfix("+");
		namespace.internInfix("-");
		namespace.internInfix("*");
		namespace.internInfix("/");

		Namespace.setCurrent(namespace);
    	Parser parser = Parboiled.createParser(Parser.class);
        while (true) {
            System.out.print("Enter a Prolog term followed by a dot (single RETURN to exit)!\n");
            String input = new Scanner(System.in).nextLine();
            if (StringUtils.isEmpty(input)) break;

            ParseRunner<Object> runner = new ReportingParseRunner<Object>(parser.Clause());
            ParsingResult<Object> result = runner.run(input);
            System.out.println("Parse tree: ");
            System.out.println(GraphUtils.printTree((GraphNode) result.parseTreeRoot, new ToStringFormatter<GraphNode>()));
            if(!result.hasErrors()) {
            	//System.out.println("Match: \"" + result.parseTreeRoot.getEndIndex());
            	System.out.println("Result: " + result.resultValue + " (" + result.resultValue.getClass() + ")");
            } else {
            	for(ParseError e : result.parseErrors) {
            		System.out.println(e + " " + e.getErrorMessage() + " " + e.getStartIndex() + " - " + e.getEndIndex());
            		if(e instanceof InvalidInputError) {
            			System.out.println("Failed matchers: " + ((InvalidInputError) e).getFailedMatchers());
            		}
            	}
            }
        }
    }
	
}